Termination w.r.t. Q of the following Term Rewriting System could not be shown:
Q restricted rewrite system:
The TRS R consists of the following rules:
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
plus(s(x), y) → plus(x, s(y))
plus(s(x), y) → s(plus(minus(x, y), double(y)))
plus(s(plus(x, y)), z) → s(plus(plus(x, y), z))
Q is empty.
↳ QTRS
Q restricted rewrite system:
The TRS R consists of the following rules:
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
plus(s(x), y) → plus(x, s(y))
plus(s(x), y) → s(plus(minus(x, y), double(y)))
plus(s(plus(x, y)), z) → s(plus(plus(x, y), z))
Q is empty.